Issue1321.agda:22,5-16
No instance of type ⊥ was found in scope.
when checking that (suc zero) is a valid argument to a function of
type (n : Nat) ⦃ _ : n ≠ zero ⦄ → Nat
